$\forall$${\it es}$:ES, ${\it Config}$:AbsInterface(chain\_config()), ${\it Cmd}$:Type, ${\it Sys}$:AbsInterface(chain\_sys(${\it Cmd}$)).
\\[0ex]${\it Sys}$(valid) $\in$ AbsInterface(chain\_sys(${\it Cmd}$))